0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 89 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 9 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 221 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇒, 0 ms)
↳27 QDP
↳28 UsableRulesReductionPairsProof (⇔, 184 ms)
↳29 QDP
↳30 PisEmptyProof (⇔, 0 ms)
↳31 YES
slowsortE_in_ga([], []) → slowsortE_out_ga([], [])
slowsortE_in_ga(.(T16, .(T17, [])), .(T20, .(T21, []))) → U7_ga(T16, T17, T20, T21, deleteB_in_agga(T20, T16, T17, X22))
deleteB_in_agga(T41, T41, T42, T42) → deleteB_out_agga(T41, T41, T42, T42)
deleteB_in_agga(T57, T55, T56, X59) → U2_agga(T57, T55, T56, X59, deleteA_in_aga(T57, T56, X59))
deleteA_in_aga(T70, .(T70, T71), T71) → deleteA_out_aga(T70, .(T70, T71), T71)
deleteA_in_aga(T81, .(T79, T80), X88) → U1_aga(T81, T79, T80, X88, deleteA_in_aga(T81, T80, X88))
U1_aga(T81, T79, T80, X88, deleteA_out_aga(T81, T80, X88)) → deleteA_out_aga(T81, .(T79, T80), X88)
U2_agga(T57, T55, T56, X59, deleteA_out_aga(T57, T56, X59)) → deleteB_out_agga(T57, T55, T56, X59)
U7_ga(T16, T17, T20, T21, deleteB_out_agga(T20, T16, T17, X22)) → slowsortE_out_ga(.(T16, .(T17, [])), .(T20, .(T21, [])))
slowsortE_in_ga(.(T16, .(T17, [])), .(T28, .(T27, []))) → U8_ga(T16, T17, T28, T27, deleteB_in_agga(T28, T16, T17, T26))
U8_ga(T16, T17, T28, T27, deleteB_out_agga(T28, T16, T17, T26)) → U9_ga(T16, T17, T28, T27, permC_in_ga(T26, T27))
permC_in_ga([], []) → permC_out_ga([], [])
permC_in_ga(.(T95, .(T96, [])), .(T99, .(T100, []))) → U3_ga(T95, T96, T99, T100, deleteB_in_agga(T99, T95, T96, X106))
U3_ga(T95, T96, T99, T100, deleteB_out_agga(T99, T95, T96, X106)) → permC_out_ga(.(T95, .(T96, [])), .(T99, .(T100, [])))
permC_in_ga(.(T95, .(T96, [])), .(T99, .(T106, []))) → U4_ga(T95, T96, T99, T106, deleteB_in_agga(T99, T95, T96, T105))
U4_ga(T95, T96, T99, T106, deleteB_out_agga(T99, T95, T96, T105)) → U5_ga(T95, T96, T99, T106, permC_in_ga(T105, T106))
U5_ga(T95, T96, T99, T106, permC_out_ga(T105, T106)) → permC_out_ga(.(T95, .(T96, [])), .(T99, .(T106, [])))
U9_ga(T16, T17, T28, T27, permC_out_ga(T26, T27)) → slowsortE_out_ga(.(T16, .(T17, [])), .(T28, .(T27, [])))
slowsortE_in_ga(.(T16, .(T17, [])), .(T118, .(T119, []))) → U10_ga(T16, T17, T118, T119, deleteB_in_agga(T118, T16, T17, T26))
U10_ga(T16, T17, T118, T119, deleteB_out_agga(T118, T16, T17, T26)) → U11_ga(T16, T17, T118, T119, permC_in_ga(T26, T119))
U11_ga(T16, T17, T118, T119, permC_out_ga(T26, T119)) → U12_ga(T16, T17, T118, T119, leD_in_ga(T118, T119))
leD_in_ga(s(T132), s(T133)) → U6_ga(T132, T133, leD_in_ga(T132, T133))
leD_in_ga(0, s(T140)) → leD_out_ga(0, s(T140))
leD_in_ga(0, 0) → leD_out_ga(0, 0)
U6_ga(T132, T133, leD_out_ga(T132, T133)) → leD_out_ga(s(T132), s(T133))
U12_ga(T16, T17, T118, T119, leD_out_ga(T118, T119)) → slowsortE_out_ga(.(T16, .(T17, [])), .(T118, .(T119, [])))
slowsortE_in_ga(.(T16, .(T17, [])), .(T118, .(T145, []))) → U13_ga(T16, T17, T118, T145, deleteB_in_agga(T118, T16, T17, T26))
U13_ga(T16, T17, T118, T145, deleteB_out_agga(T118, T16, T17, T26)) → U14_ga(T16, T17, T118, T145, permC_in_ga(T26, T145))
U14_ga(T16, T17, T118, T145, permC_out_ga(T26, T145)) → U15_ga(T16, T17, T118, T145, leD_in_ga(T118, T145))
U15_ga(T16, T17, T118, T145, leD_out_ga(T118, T145)) → slowsortE_out_ga(.(T16, .(T17, [])), .(T118, .(T145, [])))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
slowsortE_in_ga([], []) → slowsortE_out_ga([], [])
slowsortE_in_ga(.(T16, .(T17, [])), .(T20, .(T21, []))) → U7_ga(T16, T17, T20, T21, deleteB_in_agga(T20, T16, T17, X22))
deleteB_in_agga(T41, T41, T42, T42) → deleteB_out_agga(T41, T41, T42, T42)
deleteB_in_agga(T57, T55, T56, X59) → U2_agga(T57, T55, T56, X59, deleteA_in_aga(T57, T56, X59))
deleteA_in_aga(T70, .(T70, T71), T71) → deleteA_out_aga(T70, .(T70, T71), T71)
deleteA_in_aga(T81, .(T79, T80), X88) → U1_aga(T81, T79, T80, X88, deleteA_in_aga(T81, T80, X88))
U1_aga(T81, T79, T80, X88, deleteA_out_aga(T81, T80, X88)) → deleteA_out_aga(T81, .(T79, T80), X88)
U2_agga(T57, T55, T56, X59, deleteA_out_aga(T57, T56, X59)) → deleteB_out_agga(T57, T55, T56, X59)
U7_ga(T16, T17, T20, T21, deleteB_out_agga(T20, T16, T17, X22)) → slowsortE_out_ga(.(T16, .(T17, [])), .(T20, .(T21, [])))
slowsortE_in_ga(.(T16, .(T17, [])), .(T28, .(T27, []))) → U8_ga(T16, T17, T28, T27, deleteB_in_agga(T28, T16, T17, T26))
U8_ga(T16, T17, T28, T27, deleteB_out_agga(T28, T16, T17, T26)) → U9_ga(T16, T17, T28, T27, permC_in_ga(T26, T27))
permC_in_ga([], []) → permC_out_ga([], [])
permC_in_ga(.(T95, .(T96, [])), .(T99, .(T100, []))) → U3_ga(T95, T96, T99, T100, deleteB_in_agga(T99, T95, T96, X106))
U3_ga(T95, T96, T99, T100, deleteB_out_agga(T99, T95, T96, X106)) → permC_out_ga(.(T95, .(T96, [])), .(T99, .(T100, [])))
permC_in_ga(.(T95, .(T96, [])), .(T99, .(T106, []))) → U4_ga(T95, T96, T99, T106, deleteB_in_agga(T99, T95, T96, T105))
U4_ga(T95, T96, T99, T106, deleteB_out_agga(T99, T95, T96, T105)) → U5_ga(T95, T96, T99, T106, permC_in_ga(T105, T106))
U5_ga(T95, T96, T99, T106, permC_out_ga(T105, T106)) → permC_out_ga(.(T95, .(T96, [])), .(T99, .(T106, [])))
U9_ga(T16, T17, T28, T27, permC_out_ga(T26, T27)) → slowsortE_out_ga(.(T16, .(T17, [])), .(T28, .(T27, [])))
slowsortE_in_ga(.(T16, .(T17, [])), .(T118, .(T119, []))) → U10_ga(T16, T17, T118, T119, deleteB_in_agga(T118, T16, T17, T26))
U10_ga(T16, T17, T118, T119, deleteB_out_agga(T118, T16, T17, T26)) → U11_ga(T16, T17, T118, T119, permC_in_ga(T26, T119))
U11_ga(T16, T17, T118, T119, permC_out_ga(T26, T119)) → U12_ga(T16, T17, T118, T119, leD_in_ga(T118, T119))
leD_in_ga(s(T132), s(T133)) → U6_ga(T132, T133, leD_in_ga(T132, T133))
leD_in_ga(0, s(T140)) → leD_out_ga(0, s(T140))
leD_in_ga(0, 0) → leD_out_ga(0, 0)
U6_ga(T132, T133, leD_out_ga(T132, T133)) → leD_out_ga(s(T132), s(T133))
U12_ga(T16, T17, T118, T119, leD_out_ga(T118, T119)) → slowsortE_out_ga(.(T16, .(T17, [])), .(T118, .(T119, [])))
slowsortE_in_ga(.(T16, .(T17, [])), .(T118, .(T145, []))) → U13_ga(T16, T17, T118, T145, deleteB_in_agga(T118, T16, T17, T26))
U13_ga(T16, T17, T118, T145, deleteB_out_agga(T118, T16, T17, T26)) → U14_ga(T16, T17, T118, T145, permC_in_ga(T26, T145))
U14_ga(T16, T17, T118, T145, permC_out_ga(T26, T145)) → U15_ga(T16, T17, T118, T145, leD_in_ga(T118, T145))
U15_ga(T16, T17, T118, T145, leD_out_ga(T118, T145)) → slowsortE_out_ga(.(T16, .(T17, [])), .(T118, .(T145, [])))
SLOWSORTE_IN_GA(.(T16, .(T17, [])), .(T20, .(T21, []))) → U7_GA(T16, T17, T20, T21, deleteB_in_agga(T20, T16, T17, X22))
SLOWSORTE_IN_GA(.(T16, .(T17, [])), .(T20, .(T21, []))) → DELETEB_IN_AGGA(T20, T16, T17, X22)
DELETEB_IN_AGGA(T57, T55, T56, X59) → U2_AGGA(T57, T55, T56, X59, deleteA_in_aga(T57, T56, X59))
DELETEB_IN_AGGA(T57, T55, T56, X59) → DELETEA_IN_AGA(T57, T56, X59)
DELETEA_IN_AGA(T81, .(T79, T80), X88) → U1_AGA(T81, T79, T80, X88, deleteA_in_aga(T81, T80, X88))
DELETEA_IN_AGA(T81, .(T79, T80), X88) → DELETEA_IN_AGA(T81, T80, X88)
SLOWSORTE_IN_GA(.(T16, .(T17, [])), .(T28, .(T27, []))) → U8_GA(T16, T17, T28, T27, deleteB_in_agga(T28, T16, T17, T26))
U8_GA(T16, T17, T28, T27, deleteB_out_agga(T28, T16, T17, T26)) → U9_GA(T16, T17, T28, T27, permC_in_ga(T26, T27))
U8_GA(T16, T17, T28, T27, deleteB_out_agga(T28, T16, T17, T26)) → PERMC_IN_GA(T26, T27)
PERMC_IN_GA(.(T95, .(T96, [])), .(T99, .(T100, []))) → U3_GA(T95, T96, T99, T100, deleteB_in_agga(T99, T95, T96, X106))
PERMC_IN_GA(.(T95, .(T96, [])), .(T99, .(T100, []))) → DELETEB_IN_AGGA(T99, T95, T96, X106)
PERMC_IN_GA(.(T95, .(T96, [])), .(T99, .(T106, []))) → U4_GA(T95, T96, T99, T106, deleteB_in_agga(T99, T95, T96, T105))
U4_GA(T95, T96, T99, T106, deleteB_out_agga(T99, T95, T96, T105)) → U5_GA(T95, T96, T99, T106, permC_in_ga(T105, T106))
U4_GA(T95, T96, T99, T106, deleteB_out_agga(T99, T95, T96, T105)) → PERMC_IN_GA(T105, T106)
SLOWSORTE_IN_GA(.(T16, .(T17, [])), .(T118, .(T119, []))) → U10_GA(T16, T17, T118, T119, deleteB_in_agga(T118, T16, T17, T26))
U10_GA(T16, T17, T118, T119, deleteB_out_agga(T118, T16, T17, T26)) → U11_GA(T16, T17, T118, T119, permC_in_ga(T26, T119))
U10_GA(T16, T17, T118, T119, deleteB_out_agga(T118, T16, T17, T26)) → PERMC_IN_GA(T26, T119)
U11_GA(T16, T17, T118, T119, permC_out_ga(T26, T119)) → U12_GA(T16, T17, T118, T119, leD_in_ga(T118, T119))
U11_GA(T16, T17, T118, T119, permC_out_ga(T26, T119)) → LED_IN_GA(T118, T119)
LED_IN_GA(s(T132), s(T133)) → U6_GA(T132, T133, leD_in_ga(T132, T133))
LED_IN_GA(s(T132), s(T133)) → LED_IN_GA(T132, T133)
SLOWSORTE_IN_GA(.(T16, .(T17, [])), .(T118, .(T145, []))) → U13_GA(T16, T17, T118, T145, deleteB_in_agga(T118, T16, T17, T26))
U13_GA(T16, T17, T118, T145, deleteB_out_agga(T118, T16, T17, T26)) → U14_GA(T16, T17, T118, T145, permC_in_ga(T26, T145))
U13_GA(T16, T17, T118, T145, deleteB_out_agga(T118, T16, T17, T26)) → PERMC_IN_GA(T26, T145)
U14_GA(T16, T17, T118, T145, permC_out_ga(T26, T145)) → U15_GA(T16, T17, T118, T145, leD_in_ga(T118, T145))
U14_GA(T16, T17, T118, T145, permC_out_ga(T26, T145)) → LED_IN_GA(T118, T145)
slowsortE_in_ga([], []) → slowsortE_out_ga([], [])
slowsortE_in_ga(.(T16, .(T17, [])), .(T20, .(T21, []))) → U7_ga(T16, T17, T20, T21, deleteB_in_agga(T20, T16, T17, X22))
deleteB_in_agga(T41, T41, T42, T42) → deleteB_out_agga(T41, T41, T42, T42)
deleteB_in_agga(T57, T55, T56, X59) → U2_agga(T57, T55, T56, X59, deleteA_in_aga(T57, T56, X59))
deleteA_in_aga(T70, .(T70, T71), T71) → deleteA_out_aga(T70, .(T70, T71), T71)
deleteA_in_aga(T81, .(T79, T80), X88) → U1_aga(T81, T79, T80, X88, deleteA_in_aga(T81, T80, X88))
U1_aga(T81, T79, T80, X88, deleteA_out_aga(T81, T80, X88)) → deleteA_out_aga(T81, .(T79, T80), X88)
U2_agga(T57, T55, T56, X59, deleteA_out_aga(T57, T56, X59)) → deleteB_out_agga(T57, T55, T56, X59)
U7_ga(T16, T17, T20, T21, deleteB_out_agga(T20, T16, T17, X22)) → slowsortE_out_ga(.(T16, .(T17, [])), .(T20, .(T21, [])))
slowsortE_in_ga(.(T16, .(T17, [])), .(T28, .(T27, []))) → U8_ga(T16, T17, T28, T27, deleteB_in_agga(T28, T16, T17, T26))
U8_ga(T16, T17, T28, T27, deleteB_out_agga(T28, T16, T17, T26)) → U9_ga(T16, T17, T28, T27, permC_in_ga(T26, T27))
permC_in_ga([], []) → permC_out_ga([], [])
permC_in_ga(.(T95, .(T96, [])), .(T99, .(T100, []))) → U3_ga(T95, T96, T99, T100, deleteB_in_agga(T99, T95, T96, X106))
U3_ga(T95, T96, T99, T100, deleteB_out_agga(T99, T95, T96, X106)) → permC_out_ga(.(T95, .(T96, [])), .(T99, .(T100, [])))
permC_in_ga(.(T95, .(T96, [])), .(T99, .(T106, []))) → U4_ga(T95, T96, T99, T106, deleteB_in_agga(T99, T95, T96, T105))
U4_ga(T95, T96, T99, T106, deleteB_out_agga(T99, T95, T96, T105)) → U5_ga(T95, T96, T99, T106, permC_in_ga(T105, T106))
U5_ga(T95, T96, T99, T106, permC_out_ga(T105, T106)) → permC_out_ga(.(T95, .(T96, [])), .(T99, .(T106, [])))
U9_ga(T16, T17, T28, T27, permC_out_ga(T26, T27)) → slowsortE_out_ga(.(T16, .(T17, [])), .(T28, .(T27, [])))
slowsortE_in_ga(.(T16, .(T17, [])), .(T118, .(T119, []))) → U10_ga(T16, T17, T118, T119, deleteB_in_agga(T118, T16, T17, T26))
U10_ga(T16, T17, T118, T119, deleteB_out_agga(T118, T16, T17, T26)) → U11_ga(T16, T17, T118, T119, permC_in_ga(T26, T119))
U11_ga(T16, T17, T118, T119, permC_out_ga(T26, T119)) → U12_ga(T16, T17, T118, T119, leD_in_ga(T118, T119))
leD_in_ga(s(T132), s(T133)) → U6_ga(T132, T133, leD_in_ga(T132, T133))
leD_in_ga(0, s(T140)) → leD_out_ga(0, s(T140))
leD_in_ga(0, 0) → leD_out_ga(0, 0)
U6_ga(T132, T133, leD_out_ga(T132, T133)) → leD_out_ga(s(T132), s(T133))
U12_ga(T16, T17, T118, T119, leD_out_ga(T118, T119)) → slowsortE_out_ga(.(T16, .(T17, [])), .(T118, .(T119, [])))
slowsortE_in_ga(.(T16, .(T17, [])), .(T118, .(T145, []))) → U13_ga(T16, T17, T118, T145, deleteB_in_agga(T118, T16, T17, T26))
U13_ga(T16, T17, T118, T145, deleteB_out_agga(T118, T16, T17, T26)) → U14_ga(T16, T17, T118, T145, permC_in_ga(T26, T145))
U14_ga(T16, T17, T118, T145, permC_out_ga(T26, T145)) → U15_ga(T16, T17, T118, T145, leD_in_ga(T118, T145))
U15_ga(T16, T17, T118, T145, leD_out_ga(T118, T145)) → slowsortE_out_ga(.(T16, .(T17, [])), .(T118, .(T145, [])))
SLOWSORTE_IN_GA(.(T16, .(T17, [])), .(T20, .(T21, []))) → U7_GA(T16, T17, T20, T21, deleteB_in_agga(T20, T16, T17, X22))
SLOWSORTE_IN_GA(.(T16, .(T17, [])), .(T20, .(T21, []))) → DELETEB_IN_AGGA(T20, T16, T17, X22)
DELETEB_IN_AGGA(T57, T55, T56, X59) → U2_AGGA(T57, T55, T56, X59, deleteA_in_aga(T57, T56, X59))
DELETEB_IN_AGGA(T57, T55, T56, X59) → DELETEA_IN_AGA(T57, T56, X59)
DELETEA_IN_AGA(T81, .(T79, T80), X88) → U1_AGA(T81, T79, T80, X88, deleteA_in_aga(T81, T80, X88))
DELETEA_IN_AGA(T81, .(T79, T80), X88) → DELETEA_IN_AGA(T81, T80, X88)
SLOWSORTE_IN_GA(.(T16, .(T17, [])), .(T28, .(T27, []))) → U8_GA(T16, T17, T28, T27, deleteB_in_agga(T28, T16, T17, T26))
U8_GA(T16, T17, T28, T27, deleteB_out_agga(T28, T16, T17, T26)) → U9_GA(T16, T17, T28, T27, permC_in_ga(T26, T27))
U8_GA(T16, T17, T28, T27, deleteB_out_agga(T28, T16, T17, T26)) → PERMC_IN_GA(T26, T27)
PERMC_IN_GA(.(T95, .(T96, [])), .(T99, .(T100, []))) → U3_GA(T95, T96, T99, T100, deleteB_in_agga(T99, T95, T96, X106))
PERMC_IN_GA(.(T95, .(T96, [])), .(T99, .(T100, []))) → DELETEB_IN_AGGA(T99, T95, T96, X106)
PERMC_IN_GA(.(T95, .(T96, [])), .(T99, .(T106, []))) → U4_GA(T95, T96, T99, T106, deleteB_in_agga(T99, T95, T96, T105))
U4_GA(T95, T96, T99, T106, deleteB_out_agga(T99, T95, T96, T105)) → U5_GA(T95, T96, T99, T106, permC_in_ga(T105, T106))
U4_GA(T95, T96, T99, T106, deleteB_out_agga(T99, T95, T96, T105)) → PERMC_IN_GA(T105, T106)
SLOWSORTE_IN_GA(.(T16, .(T17, [])), .(T118, .(T119, []))) → U10_GA(T16, T17, T118, T119, deleteB_in_agga(T118, T16, T17, T26))
U10_GA(T16, T17, T118, T119, deleteB_out_agga(T118, T16, T17, T26)) → U11_GA(T16, T17, T118, T119, permC_in_ga(T26, T119))
U10_GA(T16, T17, T118, T119, deleteB_out_agga(T118, T16, T17, T26)) → PERMC_IN_GA(T26, T119)
U11_GA(T16, T17, T118, T119, permC_out_ga(T26, T119)) → U12_GA(T16, T17, T118, T119, leD_in_ga(T118, T119))
U11_GA(T16, T17, T118, T119, permC_out_ga(T26, T119)) → LED_IN_GA(T118, T119)
LED_IN_GA(s(T132), s(T133)) → U6_GA(T132, T133, leD_in_ga(T132, T133))
LED_IN_GA(s(T132), s(T133)) → LED_IN_GA(T132, T133)
SLOWSORTE_IN_GA(.(T16, .(T17, [])), .(T118, .(T145, []))) → U13_GA(T16, T17, T118, T145, deleteB_in_agga(T118, T16, T17, T26))
U13_GA(T16, T17, T118, T145, deleteB_out_agga(T118, T16, T17, T26)) → U14_GA(T16, T17, T118, T145, permC_in_ga(T26, T145))
U13_GA(T16, T17, T118, T145, deleteB_out_agga(T118, T16, T17, T26)) → PERMC_IN_GA(T26, T145)
U14_GA(T16, T17, T118, T145, permC_out_ga(T26, T145)) → U15_GA(T16, T17, T118, T145, leD_in_ga(T118, T145))
U14_GA(T16, T17, T118, T145, permC_out_ga(T26, T145)) → LED_IN_GA(T118, T145)
slowsortE_in_ga([], []) → slowsortE_out_ga([], [])
slowsortE_in_ga(.(T16, .(T17, [])), .(T20, .(T21, []))) → U7_ga(T16, T17, T20, T21, deleteB_in_agga(T20, T16, T17, X22))
deleteB_in_agga(T41, T41, T42, T42) → deleteB_out_agga(T41, T41, T42, T42)
deleteB_in_agga(T57, T55, T56, X59) → U2_agga(T57, T55, T56, X59, deleteA_in_aga(T57, T56, X59))
deleteA_in_aga(T70, .(T70, T71), T71) → deleteA_out_aga(T70, .(T70, T71), T71)
deleteA_in_aga(T81, .(T79, T80), X88) → U1_aga(T81, T79, T80, X88, deleteA_in_aga(T81, T80, X88))
U1_aga(T81, T79, T80, X88, deleteA_out_aga(T81, T80, X88)) → deleteA_out_aga(T81, .(T79, T80), X88)
U2_agga(T57, T55, T56, X59, deleteA_out_aga(T57, T56, X59)) → deleteB_out_agga(T57, T55, T56, X59)
U7_ga(T16, T17, T20, T21, deleteB_out_agga(T20, T16, T17, X22)) → slowsortE_out_ga(.(T16, .(T17, [])), .(T20, .(T21, [])))
slowsortE_in_ga(.(T16, .(T17, [])), .(T28, .(T27, []))) → U8_ga(T16, T17, T28, T27, deleteB_in_agga(T28, T16, T17, T26))
U8_ga(T16, T17, T28, T27, deleteB_out_agga(T28, T16, T17, T26)) → U9_ga(T16, T17, T28, T27, permC_in_ga(T26, T27))
permC_in_ga([], []) → permC_out_ga([], [])
permC_in_ga(.(T95, .(T96, [])), .(T99, .(T100, []))) → U3_ga(T95, T96, T99, T100, deleteB_in_agga(T99, T95, T96, X106))
U3_ga(T95, T96, T99, T100, deleteB_out_agga(T99, T95, T96, X106)) → permC_out_ga(.(T95, .(T96, [])), .(T99, .(T100, [])))
permC_in_ga(.(T95, .(T96, [])), .(T99, .(T106, []))) → U4_ga(T95, T96, T99, T106, deleteB_in_agga(T99, T95, T96, T105))
U4_ga(T95, T96, T99, T106, deleteB_out_agga(T99, T95, T96, T105)) → U5_ga(T95, T96, T99, T106, permC_in_ga(T105, T106))
U5_ga(T95, T96, T99, T106, permC_out_ga(T105, T106)) → permC_out_ga(.(T95, .(T96, [])), .(T99, .(T106, [])))
U9_ga(T16, T17, T28, T27, permC_out_ga(T26, T27)) → slowsortE_out_ga(.(T16, .(T17, [])), .(T28, .(T27, [])))
slowsortE_in_ga(.(T16, .(T17, [])), .(T118, .(T119, []))) → U10_ga(T16, T17, T118, T119, deleteB_in_agga(T118, T16, T17, T26))
U10_ga(T16, T17, T118, T119, deleteB_out_agga(T118, T16, T17, T26)) → U11_ga(T16, T17, T118, T119, permC_in_ga(T26, T119))
U11_ga(T16, T17, T118, T119, permC_out_ga(T26, T119)) → U12_ga(T16, T17, T118, T119, leD_in_ga(T118, T119))
leD_in_ga(s(T132), s(T133)) → U6_ga(T132, T133, leD_in_ga(T132, T133))
leD_in_ga(0, s(T140)) → leD_out_ga(0, s(T140))
leD_in_ga(0, 0) → leD_out_ga(0, 0)
U6_ga(T132, T133, leD_out_ga(T132, T133)) → leD_out_ga(s(T132), s(T133))
U12_ga(T16, T17, T118, T119, leD_out_ga(T118, T119)) → slowsortE_out_ga(.(T16, .(T17, [])), .(T118, .(T119, [])))
slowsortE_in_ga(.(T16, .(T17, [])), .(T118, .(T145, []))) → U13_ga(T16, T17, T118, T145, deleteB_in_agga(T118, T16, T17, T26))
U13_ga(T16, T17, T118, T145, deleteB_out_agga(T118, T16, T17, T26)) → U14_ga(T16, T17, T118, T145, permC_in_ga(T26, T145))
U14_ga(T16, T17, T118, T145, permC_out_ga(T26, T145)) → U15_ga(T16, T17, T118, T145, leD_in_ga(T118, T145))
U15_ga(T16, T17, T118, T145, leD_out_ga(T118, T145)) → slowsortE_out_ga(.(T16, .(T17, [])), .(T118, .(T145, [])))
LED_IN_GA(s(T132), s(T133)) → LED_IN_GA(T132, T133)
slowsortE_in_ga([], []) → slowsortE_out_ga([], [])
slowsortE_in_ga(.(T16, .(T17, [])), .(T20, .(T21, []))) → U7_ga(T16, T17, T20, T21, deleteB_in_agga(T20, T16, T17, X22))
deleteB_in_agga(T41, T41, T42, T42) → deleteB_out_agga(T41, T41, T42, T42)
deleteB_in_agga(T57, T55, T56, X59) → U2_agga(T57, T55, T56, X59, deleteA_in_aga(T57, T56, X59))
deleteA_in_aga(T70, .(T70, T71), T71) → deleteA_out_aga(T70, .(T70, T71), T71)
deleteA_in_aga(T81, .(T79, T80), X88) → U1_aga(T81, T79, T80, X88, deleteA_in_aga(T81, T80, X88))
U1_aga(T81, T79, T80, X88, deleteA_out_aga(T81, T80, X88)) → deleteA_out_aga(T81, .(T79, T80), X88)
U2_agga(T57, T55, T56, X59, deleteA_out_aga(T57, T56, X59)) → deleteB_out_agga(T57, T55, T56, X59)
U7_ga(T16, T17, T20, T21, deleteB_out_agga(T20, T16, T17, X22)) → slowsortE_out_ga(.(T16, .(T17, [])), .(T20, .(T21, [])))
slowsortE_in_ga(.(T16, .(T17, [])), .(T28, .(T27, []))) → U8_ga(T16, T17, T28, T27, deleteB_in_agga(T28, T16, T17, T26))
U8_ga(T16, T17, T28, T27, deleteB_out_agga(T28, T16, T17, T26)) → U9_ga(T16, T17, T28, T27, permC_in_ga(T26, T27))
permC_in_ga([], []) → permC_out_ga([], [])
permC_in_ga(.(T95, .(T96, [])), .(T99, .(T100, []))) → U3_ga(T95, T96, T99, T100, deleteB_in_agga(T99, T95, T96, X106))
U3_ga(T95, T96, T99, T100, deleteB_out_agga(T99, T95, T96, X106)) → permC_out_ga(.(T95, .(T96, [])), .(T99, .(T100, [])))
permC_in_ga(.(T95, .(T96, [])), .(T99, .(T106, []))) → U4_ga(T95, T96, T99, T106, deleteB_in_agga(T99, T95, T96, T105))
U4_ga(T95, T96, T99, T106, deleteB_out_agga(T99, T95, T96, T105)) → U5_ga(T95, T96, T99, T106, permC_in_ga(T105, T106))
U5_ga(T95, T96, T99, T106, permC_out_ga(T105, T106)) → permC_out_ga(.(T95, .(T96, [])), .(T99, .(T106, [])))
U9_ga(T16, T17, T28, T27, permC_out_ga(T26, T27)) → slowsortE_out_ga(.(T16, .(T17, [])), .(T28, .(T27, [])))
slowsortE_in_ga(.(T16, .(T17, [])), .(T118, .(T119, []))) → U10_ga(T16, T17, T118, T119, deleteB_in_agga(T118, T16, T17, T26))
U10_ga(T16, T17, T118, T119, deleteB_out_agga(T118, T16, T17, T26)) → U11_ga(T16, T17, T118, T119, permC_in_ga(T26, T119))
U11_ga(T16, T17, T118, T119, permC_out_ga(T26, T119)) → U12_ga(T16, T17, T118, T119, leD_in_ga(T118, T119))
leD_in_ga(s(T132), s(T133)) → U6_ga(T132, T133, leD_in_ga(T132, T133))
leD_in_ga(0, s(T140)) → leD_out_ga(0, s(T140))
leD_in_ga(0, 0) → leD_out_ga(0, 0)
U6_ga(T132, T133, leD_out_ga(T132, T133)) → leD_out_ga(s(T132), s(T133))
U12_ga(T16, T17, T118, T119, leD_out_ga(T118, T119)) → slowsortE_out_ga(.(T16, .(T17, [])), .(T118, .(T119, [])))
slowsortE_in_ga(.(T16, .(T17, [])), .(T118, .(T145, []))) → U13_ga(T16, T17, T118, T145, deleteB_in_agga(T118, T16, T17, T26))
U13_ga(T16, T17, T118, T145, deleteB_out_agga(T118, T16, T17, T26)) → U14_ga(T16, T17, T118, T145, permC_in_ga(T26, T145))
U14_ga(T16, T17, T118, T145, permC_out_ga(T26, T145)) → U15_ga(T16, T17, T118, T145, leD_in_ga(T118, T145))
U15_ga(T16, T17, T118, T145, leD_out_ga(T118, T145)) → slowsortE_out_ga(.(T16, .(T17, [])), .(T118, .(T145, [])))
LED_IN_GA(s(T132), s(T133)) → LED_IN_GA(T132, T133)
LED_IN_GA(s(T132)) → LED_IN_GA(T132)
From the DPs we obtained the following set of size-change graphs:
DELETEA_IN_AGA(T81, .(T79, T80), X88) → DELETEA_IN_AGA(T81, T80, X88)
slowsortE_in_ga([], []) → slowsortE_out_ga([], [])
slowsortE_in_ga(.(T16, .(T17, [])), .(T20, .(T21, []))) → U7_ga(T16, T17, T20, T21, deleteB_in_agga(T20, T16, T17, X22))
deleteB_in_agga(T41, T41, T42, T42) → deleteB_out_agga(T41, T41, T42, T42)
deleteB_in_agga(T57, T55, T56, X59) → U2_agga(T57, T55, T56, X59, deleteA_in_aga(T57, T56, X59))
deleteA_in_aga(T70, .(T70, T71), T71) → deleteA_out_aga(T70, .(T70, T71), T71)
deleteA_in_aga(T81, .(T79, T80), X88) → U1_aga(T81, T79, T80, X88, deleteA_in_aga(T81, T80, X88))
U1_aga(T81, T79, T80, X88, deleteA_out_aga(T81, T80, X88)) → deleteA_out_aga(T81, .(T79, T80), X88)
U2_agga(T57, T55, T56, X59, deleteA_out_aga(T57, T56, X59)) → deleteB_out_agga(T57, T55, T56, X59)
U7_ga(T16, T17, T20, T21, deleteB_out_agga(T20, T16, T17, X22)) → slowsortE_out_ga(.(T16, .(T17, [])), .(T20, .(T21, [])))
slowsortE_in_ga(.(T16, .(T17, [])), .(T28, .(T27, []))) → U8_ga(T16, T17, T28, T27, deleteB_in_agga(T28, T16, T17, T26))
U8_ga(T16, T17, T28, T27, deleteB_out_agga(T28, T16, T17, T26)) → U9_ga(T16, T17, T28, T27, permC_in_ga(T26, T27))
permC_in_ga([], []) → permC_out_ga([], [])
permC_in_ga(.(T95, .(T96, [])), .(T99, .(T100, []))) → U3_ga(T95, T96, T99, T100, deleteB_in_agga(T99, T95, T96, X106))
U3_ga(T95, T96, T99, T100, deleteB_out_agga(T99, T95, T96, X106)) → permC_out_ga(.(T95, .(T96, [])), .(T99, .(T100, [])))
permC_in_ga(.(T95, .(T96, [])), .(T99, .(T106, []))) → U4_ga(T95, T96, T99, T106, deleteB_in_agga(T99, T95, T96, T105))
U4_ga(T95, T96, T99, T106, deleteB_out_agga(T99, T95, T96, T105)) → U5_ga(T95, T96, T99, T106, permC_in_ga(T105, T106))
U5_ga(T95, T96, T99, T106, permC_out_ga(T105, T106)) → permC_out_ga(.(T95, .(T96, [])), .(T99, .(T106, [])))
U9_ga(T16, T17, T28, T27, permC_out_ga(T26, T27)) → slowsortE_out_ga(.(T16, .(T17, [])), .(T28, .(T27, [])))
slowsortE_in_ga(.(T16, .(T17, [])), .(T118, .(T119, []))) → U10_ga(T16, T17, T118, T119, deleteB_in_agga(T118, T16, T17, T26))
U10_ga(T16, T17, T118, T119, deleteB_out_agga(T118, T16, T17, T26)) → U11_ga(T16, T17, T118, T119, permC_in_ga(T26, T119))
U11_ga(T16, T17, T118, T119, permC_out_ga(T26, T119)) → U12_ga(T16, T17, T118, T119, leD_in_ga(T118, T119))
leD_in_ga(s(T132), s(T133)) → U6_ga(T132, T133, leD_in_ga(T132, T133))
leD_in_ga(0, s(T140)) → leD_out_ga(0, s(T140))
leD_in_ga(0, 0) → leD_out_ga(0, 0)
U6_ga(T132, T133, leD_out_ga(T132, T133)) → leD_out_ga(s(T132), s(T133))
U12_ga(T16, T17, T118, T119, leD_out_ga(T118, T119)) → slowsortE_out_ga(.(T16, .(T17, [])), .(T118, .(T119, [])))
slowsortE_in_ga(.(T16, .(T17, [])), .(T118, .(T145, []))) → U13_ga(T16, T17, T118, T145, deleteB_in_agga(T118, T16, T17, T26))
U13_ga(T16, T17, T118, T145, deleteB_out_agga(T118, T16, T17, T26)) → U14_ga(T16, T17, T118, T145, permC_in_ga(T26, T145))
U14_ga(T16, T17, T118, T145, permC_out_ga(T26, T145)) → U15_ga(T16, T17, T118, T145, leD_in_ga(T118, T145))
U15_ga(T16, T17, T118, T145, leD_out_ga(T118, T145)) → slowsortE_out_ga(.(T16, .(T17, [])), .(T118, .(T145, [])))
DELETEA_IN_AGA(T81, .(T79, T80), X88) → DELETEA_IN_AGA(T81, T80, X88)
DELETEA_IN_AGA(.(T79, T80)) → DELETEA_IN_AGA(T80)
From the DPs we obtained the following set of size-change graphs:
PERMC_IN_GA(.(T95, .(T96, [])), .(T99, .(T106, []))) → U4_GA(T95, T96, T99, T106, deleteB_in_agga(T99, T95, T96, T105))
U4_GA(T95, T96, T99, T106, deleteB_out_agga(T99, T95, T96, T105)) → PERMC_IN_GA(T105, T106)
slowsortE_in_ga([], []) → slowsortE_out_ga([], [])
slowsortE_in_ga(.(T16, .(T17, [])), .(T20, .(T21, []))) → U7_ga(T16, T17, T20, T21, deleteB_in_agga(T20, T16, T17, X22))
deleteB_in_agga(T41, T41, T42, T42) → deleteB_out_agga(T41, T41, T42, T42)
deleteB_in_agga(T57, T55, T56, X59) → U2_agga(T57, T55, T56, X59, deleteA_in_aga(T57, T56, X59))
deleteA_in_aga(T70, .(T70, T71), T71) → deleteA_out_aga(T70, .(T70, T71), T71)
deleteA_in_aga(T81, .(T79, T80), X88) → U1_aga(T81, T79, T80, X88, deleteA_in_aga(T81, T80, X88))
U1_aga(T81, T79, T80, X88, deleteA_out_aga(T81, T80, X88)) → deleteA_out_aga(T81, .(T79, T80), X88)
U2_agga(T57, T55, T56, X59, deleteA_out_aga(T57, T56, X59)) → deleteB_out_agga(T57, T55, T56, X59)
U7_ga(T16, T17, T20, T21, deleteB_out_agga(T20, T16, T17, X22)) → slowsortE_out_ga(.(T16, .(T17, [])), .(T20, .(T21, [])))
slowsortE_in_ga(.(T16, .(T17, [])), .(T28, .(T27, []))) → U8_ga(T16, T17, T28, T27, deleteB_in_agga(T28, T16, T17, T26))
U8_ga(T16, T17, T28, T27, deleteB_out_agga(T28, T16, T17, T26)) → U9_ga(T16, T17, T28, T27, permC_in_ga(T26, T27))
permC_in_ga([], []) → permC_out_ga([], [])
permC_in_ga(.(T95, .(T96, [])), .(T99, .(T100, []))) → U3_ga(T95, T96, T99, T100, deleteB_in_agga(T99, T95, T96, X106))
U3_ga(T95, T96, T99, T100, deleteB_out_agga(T99, T95, T96, X106)) → permC_out_ga(.(T95, .(T96, [])), .(T99, .(T100, [])))
permC_in_ga(.(T95, .(T96, [])), .(T99, .(T106, []))) → U4_ga(T95, T96, T99, T106, deleteB_in_agga(T99, T95, T96, T105))
U4_ga(T95, T96, T99, T106, deleteB_out_agga(T99, T95, T96, T105)) → U5_ga(T95, T96, T99, T106, permC_in_ga(T105, T106))
U5_ga(T95, T96, T99, T106, permC_out_ga(T105, T106)) → permC_out_ga(.(T95, .(T96, [])), .(T99, .(T106, [])))
U9_ga(T16, T17, T28, T27, permC_out_ga(T26, T27)) → slowsortE_out_ga(.(T16, .(T17, [])), .(T28, .(T27, [])))
slowsortE_in_ga(.(T16, .(T17, [])), .(T118, .(T119, []))) → U10_ga(T16, T17, T118, T119, deleteB_in_agga(T118, T16, T17, T26))
U10_ga(T16, T17, T118, T119, deleteB_out_agga(T118, T16, T17, T26)) → U11_ga(T16, T17, T118, T119, permC_in_ga(T26, T119))
U11_ga(T16, T17, T118, T119, permC_out_ga(T26, T119)) → U12_ga(T16, T17, T118, T119, leD_in_ga(T118, T119))
leD_in_ga(s(T132), s(T133)) → U6_ga(T132, T133, leD_in_ga(T132, T133))
leD_in_ga(0, s(T140)) → leD_out_ga(0, s(T140))
leD_in_ga(0, 0) → leD_out_ga(0, 0)
U6_ga(T132, T133, leD_out_ga(T132, T133)) → leD_out_ga(s(T132), s(T133))
U12_ga(T16, T17, T118, T119, leD_out_ga(T118, T119)) → slowsortE_out_ga(.(T16, .(T17, [])), .(T118, .(T119, [])))
slowsortE_in_ga(.(T16, .(T17, [])), .(T118, .(T145, []))) → U13_ga(T16, T17, T118, T145, deleteB_in_agga(T118, T16, T17, T26))
U13_ga(T16, T17, T118, T145, deleteB_out_agga(T118, T16, T17, T26)) → U14_ga(T16, T17, T118, T145, permC_in_ga(T26, T145))
U14_ga(T16, T17, T118, T145, permC_out_ga(T26, T145)) → U15_ga(T16, T17, T118, T145, leD_in_ga(T118, T145))
U15_ga(T16, T17, T118, T145, leD_out_ga(T118, T145)) → slowsortE_out_ga(.(T16, .(T17, [])), .(T118, .(T145, [])))
PERMC_IN_GA(.(T95, .(T96, [])), .(T99, .(T106, []))) → U4_GA(T95, T96, T99, T106, deleteB_in_agga(T99, T95, T96, T105))
U4_GA(T95, T96, T99, T106, deleteB_out_agga(T99, T95, T96, T105)) → PERMC_IN_GA(T105, T106)
deleteB_in_agga(T41, T41, T42, T42) → deleteB_out_agga(T41, T41, T42, T42)
deleteB_in_agga(T57, T55, T56, X59) → U2_agga(T57, T55, T56, X59, deleteA_in_aga(T57, T56, X59))
U2_agga(T57, T55, T56, X59, deleteA_out_aga(T57, T56, X59)) → deleteB_out_agga(T57, T55, T56, X59)
deleteA_in_aga(T70, .(T70, T71), T71) → deleteA_out_aga(T70, .(T70, T71), T71)
deleteA_in_aga(T81, .(T79, T80), X88) → U1_aga(T81, T79, T80, X88, deleteA_in_aga(T81, T80, X88))
U1_aga(T81, T79, T80, X88, deleteA_out_aga(T81, T80, X88)) → deleteA_out_aga(T81, .(T79, T80), X88)
PERMC_IN_GA(.(T95, .(T96, []))) → U4_GA(deleteB_in_agga(T95, T96))
U4_GA(deleteB_out_agga(T99, T105)) → PERMC_IN_GA(T105)
deleteB_in_agga(T41, T42) → deleteB_out_agga(T41, T42)
deleteB_in_agga(T55, T56) → U2_agga(deleteA_in_aga(T56))
U2_agga(deleteA_out_aga(T57, X59)) → deleteB_out_agga(T57, X59)
deleteA_in_aga(.(T70, T71)) → deleteA_out_aga(T70, T71)
deleteA_in_aga(.(T79, T80)) → U1_aga(deleteA_in_aga(T80))
U1_aga(deleteA_out_aga(T81, X88)) → deleteA_out_aga(T81, X88)
deleteB_in_agga(x0, x1)
U2_agga(x0)
deleteA_in_aga(x0)
U1_aga(x0)
The following rules are removed from R:
PERMC_IN_GA(.(T95, .(T96, []))) → U4_GA(deleteB_in_agga(T95, T96))
U4_GA(deleteB_out_agga(T99, T105)) → PERMC_IN_GA(T105)
Used ordering: POLO with Polynomial interpretation [POLO]:
deleteB_in_agga(T41, T42) → deleteB_out_agga(T41, T42)
U2_agga(deleteA_out_aga(T57, X59)) → deleteB_out_agga(T57, X59)
deleteA_in_aga(.(T70, T71)) → deleteA_out_aga(T70, T71)
deleteA_in_aga(.(T79, T80)) → U1_aga(deleteA_in_aga(T80))
U1_aga(deleteA_out_aga(T81, X88)) → deleteA_out_aga(T81, X88)
POL(.(x1, x2)) = 1 + 2·x1 + 2·x2
POL(PERMC_IN_GA(x1)) = 1 + x1
POL(U1_aga(x1)) = 1 + x1
POL(U2_agga(x1)) = 2 + x1
POL(U4_GA(x1)) = 2·x1
POL([]) = 0
POL(deleteA_in_aga(x1)) = x1
POL(deleteA_out_aga(x1, x2)) = x1 + 2·x2
POL(deleteB_in_agga(x1, x2)) = 2 + x1 + 2·x2
POL(deleteB_out_agga(x1, x2)) = 1 + x1 + 2·x2
deleteB_in_agga(T55, T56) → U2_agga(deleteA_in_aga(T56))
deleteB_in_agga(x0, x1)
U2_agga(x0)
deleteA_in_aga(x0)
U1_aga(x0)